\begin{tabbing}
$\forall$$i$, $x$:Id, $a$, $b$:Knd, $T$:Type.
\\[0ex]@$i$: only members of [$a$; $b$] affect $x$ :$T$ $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: only members of [$a$; $b$] affect $x$ :$T$ $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]vartype($i$;$x$) $\subseteq\rho$ $T$
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]($\neg$($x$ after $e$) $=$ ($x$ when $e$) $\in$ $T$ $\Rightarrow$ kind($e$) $=$ $a$ $\in$ Knd $\vee$ kind($e$) $=$ $b$ $\in$ Knd)
\\[0ex]\& ($\neg$kind($e$) $=$ $a$ $\Rightarrow$ $\neg$kind($e$) $=$ $b$ $\in$ Knd $\Rightarrow$ ($x$ after $e$) $=$ ($x$ when $e$) $\in$ $T$))
\-\-\-
\end{tabbing}